r:Rng, p, q:, E:({p..q}|r|). ((r) p  i < q. E(i))  |r| 

latex

Up	rings 1
Definitions of Statement	Rng, r+gp, (r) i  k < j. E(k)
Definitions	t.1, x. t(x), |g|, IMonoid, r+gp, x(s), (r) i  k < j. E(k), t  T, x:A. B(x), , P & Q, Mon, Group{i}, AbGrp, Rng
Lemmas	rng wf, add grp of rng wf, int seg wf, rng car wf, abgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, mon itop wf